es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C, e, e':E.
f2f+-pred(e,e')
 (([e: sndr is_req   rcvr]  [e': rcvr is_ack  sndr])
 & ([e: rcvr is_ack  sndr]  [e': sndr is_req   rcvr])) 

latex

Definitions	x:A. B(x), is_ack , t  T, [e: i p j], P  Q, is_req  , P  Q, P & Q, f2f+-pred(e',e), ES, FIFO, F2F+-decls, ff.C, E, left + right, x:A  B(x), A c B, x:A. B(x), False, ff.Sender, f(a), s = t, , s ~ t, {T}, SQType(T), let x,y = A in B(x;y), t.1, A
Lemmas	snd-it-of-rcv-it, f2f+-pred wf, es-E wf, fifoC wf, F2F+-decls wf, FIFO wf, event system wf, f2f+-property, f2f+Req wf, snd-it wf, f2f+Ack wf